/*//////////////////////////////////////////////////////////////////////////////
// This file is part of the Mist compiler.                                    //
//                                                                            //
// Copyright (C) 2009, 2010 The Mist project                                  //
//                                                                            //
// For a list of contributors, see the COMMITTERS file.                       //
//                                                                            //
// The Mist compiler is free software: you can redistribute it and/or modify  //
// it under the terms of the GNU General Public License as published by       //
// the Free Software Foundation, either version 3 of the License, or          //
// (at your option) any later version.                                        //
//                                                                            //
// The Mist compiler is distributed in the hope that it will be useful,       //
// but WITHOUT ANY WARRANTY; without even the implied warranty of             //
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the              //
// GNU General Public License for more details.                               //
//                                                                            //
// You should have received a copy of the GNU General Public License          //
// in the COPYING file. If not, see <http://www.gnu.org/licenses/>.           //
//////////////////////////////////////////////////////////////////////////////*/

/**
/// \file
/// A Flex file, describing the lexical structure of Mist.
/// The generated lexer source-code should only be used by the parse.hpp
/// file, which encapsulates this functionality.
**/

/*//////////////////////////////////////////////////////////////////////////////
// Initial Code                                                               //
//////////////////////////////////////////////////////////////////////////////*/

%top {
	#include <string>
	using std::string;
	
	#include <istream>
	using std::istream;
	
	#include <sstream>
	using std::ostringstream;
	
	#include <climits>
	
	#include "common/bigint.hpp"
	#include "common/ptr.hpp"
	#include "common/types.hpp"
	#include "codestream.hpp"
	#include "messages.hpp"
	#include "operator.hpp"
	#include "parser.tab.hpp"
	
	struct LexerParams {
		istream* in;
		wptr<Messages> messages;
		int entry_point;
	};
	
	#define YY_INPUT(buf, result, max_size) { \
		yyextra->in->get(buf, max_size, EOF); \
		result = yyextra->in->gcount();       \
	}
	
	#define COLUMNS do { yylloc->step();          \
	                     yylloc->columns(yyleng); \
	                } while (false)
	
	#define LINES   do { yylloc->step();        \
	                     yylloc->lines(yyleng); \
	                     yylloc->columns(1);    \
	                } while (false)
}

/*//////////////////////////////////////////////////////////////////////////////
// Options                                                                    //
//////////////////////////////////////////////////////////////////////////////*/

%option outfile=    "lexer.lex.cpp"
%option header-file="lexer.lex.hpp"
%option reentrant
%option noyywrap
%option nounput
%option 8bit
%option extra-type="LexerParams*"
%option nostdinit
%option noyylineno
%option bison-bridge
%option bison-locations
%option pointer
%option nounistd
%option nodefault

/*//////////////////////////////////////////////////////////////////////////////
// Start Conditions                                                           //
//////////////////////////////////////////////////////////////////////////////*/

%x LINE_COMMENT
%x BLOCK_COMMENT
%x NESTING_COMMENT
%x STR_LITERAL
%s ASSERTION_AREA

/*//////////////////////////////////////////////////////////////////////////////
// Regex Definitions                                                          //
//////////////////////////////////////////////////////////////////////////////*/

identifier    [_a-zA-Z][_a-zA-Z0-9]*
decimalnumber [0-9][0-9]*
binarynumber  0[bB][01][01]*
hexnumber     0[xX][0-9a-fA-F][0-9a-fA-F]*
octalnumber   0[oOqQ][0-7][0-7]*
truthvalue    true|false
implop        "<==>"|"<=="|"==>"
relop         "<>="|"<="|"<>"|">="|"<"|">"|"="

%%

 /*/////////////////////////////////////////////////////////////////////////////
 // Some In-Function Code                                                     //
 /////////////////////////////////////////////////////////////////////////////*/

%{
	typedef yy::Parser::token token;
	
	uint nestingCommentDepth = 0;
	uint bracketDepth = 0;
	int returnState = INITIAL;
	string str;
	
	// If we are only just beginning to scan the input,
	// send the entrypoint token first, which the parser
	// uses to simulate multiple entrypoints in the grammar.
	//
	if (yyextra->entry_point != 0) {
		int entry_point = yyextra->entry_point;
		yyextra->entry_point = 0;
		return entry_point;
	}
%}

 /*/////////////////////////////////////////////////////////////////////////////
 // Lexer Tokens                                                              //
 /////////////////////////////////////////////////////////////////////////////*/

 /*------------language-constructs----------------*/

if    { COLUMNS;
        return token::IF;
      }

else  { COLUMNS;
        return token::ELSE;
      }

while { COLUMNS;
        return token::WHILE;
      }

for   { COLUMNS;
        return token::FOR;
      }

".."  { COLUMNS;
        return token::INTERVAL_OP;
      }

void  { COLUMNS;
        return token::VOID;
      }

pre   { COLUMNS;
        return token::PRE;
      }

post  { COLUMNS;
        return token::POST;
      }

logical { COLUMNS;
          return token::LOGICAL;
        }

body  { COLUMNS;
        return token::BODY;
      }

bound { COLUMNS;
        return token::BOUND;
      }

oldbound { COLUMNS;
           return token::OLDBOUND;
         }

do    { COLUMNS;
        return token::DO;
      }

invariant { COLUMNS;
            return token::INVARIANT;
          }

"<->" { COLUMNS;
        return token::SWAP_OP;
      }

"<-"  { COLUMNS;
        return token::ASSIGN_OP;
      }

mod   { COLUMNS;
        return token::MOD_OP;
      }

cpp   { COLUMNS;
        return token::CPP;
      }

KeY   { COLUMNS;
        return token::KEY;
      }

type  { COLUMNS;
        return token::TYPE;
      }

new   { COLUMNS;
        return token::NEW;
      }

ensure { COLUMNS;
         return token::ENSURE;
       }

[%]{decimalnumber} { COLUMNS;
                     yylval->t_small_int = BigInt(yytext + 1, 10).get_ui();
                     return token::PLACEHOLDER;
                   }

[!]*and       { COLUMNS;
                uint i = 0;
                if (yytext[i] == '!') {
                	yylval->t_composite_operator = n_sptr_ptr(new CompositeOperator(n_sptr(new SingleOperator("! 1"))));
                	while (yytext[++i] == '!')
                		(*yylval->t_composite_operator)->add(n_sptr(new SingleOperator("! 1")));
                	(*yylval->t_composite_operator)->add(n_sptr(new SingleOperator("1 " + string(yytext + i) + " 2")));
                } else {
                	yylval->t_composite_operator = n_sptr_ptr(new CompositeOperator(n_sptr(new SingleOperator("1 " + string(yytext) + " 2"))));
                }
                return token::AND_OP;
              }

[!]*or        { COLUMNS;
                uint i = 0;
                if (yytext[i] == '!') {
                	yylval->t_composite_operator = n_sptr_ptr(new CompositeOperator(n_sptr(new SingleOperator("! 1"))));
                	while (yytext[++i] == '!')
                		(*yylval->t_composite_operator)->add(n_sptr(new SingleOperator("! 1")));
                	(*yylval->t_composite_operator)->add(n_sptr(new SingleOperator("1 " + string(yytext + i) + " 2")));
                } else {
                	yylval->t_composite_operator = n_sptr_ptr(new CompositeOperator(n_sptr(new SingleOperator("1 " + string(yytext) + " 2"))));
                }
                return token::OR_OP;
              }

[!]*{implop}  { COLUMNS;
                uint i = 0;
                if (yytext[i] == '!') {
                	yylval->t_composite_operator = n_sptr_ptr(new CompositeOperator(n_sptr(new SingleOperator("! 1"))));
                	while (yytext[++i] == '!')
                		(*yylval->t_composite_operator)->add(n_sptr(new SingleOperator("! 1")));
                	(*yylval->t_composite_operator)->add(n_sptr(new SingleOperator("1 " + string(yytext + i) + " 2")));
                } else {
                	yylval->t_composite_operator = n_sptr_ptr(new CompositeOperator(n_sptr(new SingleOperator("1 " + string(yytext) + " 2"))));
                }
                return token::IMPLICATION_OP;
              }

[!]*{relop}   { COLUMNS;
                uint i = 0;
                if (yytext[i] == '!') {
                	yylval->t_composite_operator = n_sptr_ptr(new CompositeOperator(n_sptr(new SingleOperator("! 1"))));
                	while (yytext[++i] == '!')
                		(*yylval->t_composite_operator)->add(n_sptr(new SingleOperator("! 1")));
                	(*yylval->t_composite_operator)->add(n_sptr(new SingleOperator("1 " + string(yytext + i) + " 2")));
                } else {
                	yylval->t_composite_operator = n_sptr_ptr(new CompositeOperator(n_sptr(new SingleOperator("1 " + string(yytext) + " 2"))));
                }
                return token::RELATION_OP;
              }

 /*------------literals--------------------------*/

{decimalnumber} { COLUMNS;
                  yylval->t_int = new BigInt(yytext, 10);
                  return token::NUMBER;
                }

{binarynumber}  { COLUMNS;
                  yylval->t_int = new BigInt(yytext + 2, 2);
                  return token::NUMBER;
                }

{hexnumber}     { COLUMNS;
                  yylval->t_int = new BigInt(yytext + 2, 16);
                  return token::NUMBER;
                }

{octalnumber}   { COLUMNS;
                  yylval->t_int = new BigInt(yytext + 2, 8);
                  return token::NUMBER;
                }

{truthvalue}    { COLUMNS;
                  yylval->t_bool = (yytext[0] == 't');
                  return token::TRUTH_VALUE;
                }

 /*------------string literal--------------------*/

\" { yylloc->step();
     yylloc->columns(yyleng);
     str = "";
     BEGIN(STR_LITERAL);
   }

<STR_LITERAL>{
	
	\" { yylloc->columns(yyleng);
	     yylval->t_string = new string(str);
	     BEGIN(INITIAL);
	     return token::STRING_LITERAL;
	   }
	
	[^\n\"\\]+ { yylloc->columns(yyleng);
	             str += string(yytext);
	           }
	
	\n+ { yylloc->lines(yyleng);
	      yylloc->columns(1);
	      str += string(yytext);
	    }
	
	"\\b" { yylloc->columns(yyleng);
	        str += '\b';
	      }
	
	"\\t" { yylloc->columns(yyleng);
	        str += '\t';
	      }
	
	"\\n" { yylloc->columns(yyleng);
	        str += '\n';
	      }
	
	"\\f" { yylloc->columns(yyleng);
	        str += '\f';
	      }
	
	"\\r" { yylloc->columns(yyleng);
	        str += '\r';
	      }
	
	"\\\"" { yylloc->columns(yyleng);
	         str += '"';
	       }
	
	"\\\\" { yylloc->columns(yyleng);
	         str += '\\';
	       }
	
	\\[0-9a-fA-F][0-9a-fA-F] { yylloc->columns(yyleng);
	                           str += char(BigInt(yytext + 1, 16).get_ui());
	                         }
	
	\\. { yylloc->columns(yyleng);
	      if (yyextra->messages)
	      	yyextra->messages->add("invalid escape sequence", *yylloc);
	    }
	
	<<EOF>> { if (yyextra->messages)
	          	yyextra->messages->add("unterminated string", *yylloc);
	          return token::END;
	        }
}

 /*------------identifier------------------------*/

{identifier} { COLUMNS;
               yylval->t_string = new string(yytext);
               return token::IDENTIFIER;
             }

 /*------------assertion-------------------------*/

<INITIAL>"@"  { COLUMNS;
                returnState = ASSERTION_AREA;
                BEGIN(ASSERTION_AREA);
                return token::ASSERTION_BEGIN;
              }

<ASSERTION_AREA>{
	
	[\n]/([\t ]*[@])  { LINES;
	                    // One column for each @, space and tab until first @
	                    //
	                    yylloc->columns(1);
	                    while (yyinput(yyscanner) != '@')
	                    	yylloc->columns(1);
	                  }
	
	[\n]/([\t ]*[^\t @]) { yyless(0); // Match newline again later
	                       returnState = INITIAL;
	                       BEGIN(INITIAL);
	                       return token::ASSERTION_END;
	                     }
	
	 /* Make sure that the following {} bracket rules
	    appear before the regular bracket matching rules in this file.
	    We want to make sure that if we are in the ASSERTION_AREA
	    condition, that the following rules are always invoked
	    first, so that a line assertion may be ended with a redundant
	    closing bracket, as well as with a newline. That
	    bracket could then perhaps be matched outside the assertion.
	    Location tracking is done in the general {} rule below, which
	    is always invoked after these rules, by means of REJECT or yyless. */
	
	[\{] { assert(bracketDepth < UINT_MAX);
	       ++bracketDepth;
	       REJECT; /* Scan the { token with the other rule below */
	     }
	
	[\}]  { if (bracketDepth > 0) {
	        	--bracketDepth;
	        	REJECT; /* Scan the } token with the other rule below */
	        } else {
	        	yyless(0); /* Scan the } token again next time */
	        	returnState = INITIAL;
	        	BEGIN(INITIAL);
	        	return token::ASSERTION_END;
	        }
	      }
	
}

 /*------------line comments---------------------*/

"|" { yylloc->step();
      yylloc->columns(yyleng);
      returnState = YY_START;
      BEGIN(LINE_COMMENT);
    }

<LINE_COMMENT>{
	
	[^\n]+ { yylloc->columns(yyleng); }
	
	[\n]  { if (returnState == ASSERTION_AREA)
	        	yyless(0); // If we fall back to an assertion area,
	        	           // scan the newline again to handle it
		                   // in the appropriate context.
	        else
	        	LINES;
	        BEGIN(returnState);
	      }
	
}

 /*------------block-comment---------------------*/

"|-" { yylloc->step();
       yylloc->columns(yyleng);
       returnState = YY_START;
       BEGIN(BLOCK_COMMENT);
     }

<BLOCK_COMMENT>{
	
	<<EOF>>       { yylloc->columns(1);
	                if (yyextra->messages)
	                	yyextra->messages->add("unterminated comment", *yylloc);
	                return token::END;
	              }
	
	[^\-\n]+       { yylloc->columns(yyleng);
	              }
	
	"-"           { yylloc->columns(yyleng);
	              }
	
	[\n]+         { yylloc->lines(yyleng);
                    yylloc->columns(1);
	              }
	
	"-|"          { yylloc->columns(yyleng);
	                BEGIN(returnState);
	              }
	
}

 /*------------nesting comments------------------*/

"|+"  { COLUMNS;
        ++nestingCommentDepth;
        returnState = YY_START;
        BEGIN(NESTING_COMMENT);
      }

<NESTING_COMMENT>{
	
	<<EOF>>       { yylloc->columns(1);
	                if (yyextra->messages)
	                	yyextra->messages->add("unterminated comment", *yylloc);
	                return token::END;
	              }
	
	"|+"          { yylloc->columns(yyleng);
	                assert(nestingCommentDepth < UINT_MAX);
	                ++nestingCommentDepth;
	              }
	
	[^+|\n]+      { yylloc->columns(yyleng);
	              }
	
	"|"           { yylloc->columns(yyleng);
	              }
	
	"+"           { yylloc->columns(yyleng);
	              }
	
	[\n]+         { yylloc->lines(yyleng);
                    yylloc->columns(1);
	                if (returnState == ASSERTION_AREA) {
	                	returnState = INITIAL;
	                	return token::ASSERTION_END;
	                }
	              }
	
	"+|"          { yylloc->columns(yyleng);
	                --nestingCommentDepth;
	                if (nestingCommentDepth == 0)
	                	BEGIN(returnState);
	              }
	
}

 /*------------single character tokens-----------*/

 /* Make sure that the {} brackets of this rule remain
    textually after the more specialized matching rules
    in the ASSERTION_AREA condition. The rule here will be invoked
    anyway, the ASSERTION_AREA rules will make sure of that. */

[!?#+\-*/.;,\[\]\{\}\(\)\^`] { COLUMNS;
                               return yytext[0];
                             }

 /*------------whitespace------------------------*/

[ ]+   { COLUMNS; }

[\t]+  { COLUMNS; }

[\n]+  { LINES; }

 /*------------end of file-----------------------*/

<<EOF>> { return token::END; }

 /*------------catch-all-------------------------*/

. { COLUMNS;
    assert(yyextra->messages);
    yyextra->messages->add("unexpected character", *yylloc, string(yytext));
  }
